YES 1.846
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule List
|
| ((intersect :: Eq a => [[a]] -> [[a]] -> [[a]]) :: Eq a => [[a]] -> [[a]] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | intersect :: Eq a => [a] -> [a] -> [a]
| intersect | | = | intersectBy (==) |
|
| | intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| intersectBy | eq xs ys | = | concatMap (\vv2 ->
| case | vv2 of |
|
| x | -> | if any (eq x) ys then x : [] else [] |
|
| _ | -> | [] |
) xs |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Lambda Reductions:
The following Lambda expression
\vv2→
| case | vv2 of |
| | x | → if any (eq x) ys then x : [] else [] |
| | _ | → [] |
is transformed to
| intersectBy0 | eq ys vv2 | =
| case | vv2 of | | | x | → if any (eq x) ys then x : [] else [] |
| | _ | → [] |
|
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
mainModule List
|
| ((intersect :: Eq a => [[a]] -> [[a]] -> [[a]]) :: Eq a => [[a]] -> [[a]] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | intersect :: Eq a => [a] -> [a] -> [a]
| intersect | | = | intersectBy (==) |
|
| | intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| intersectBy | eq xs ys | = | concatMap (intersectBy0 eq ys) xs |
|
| |
| intersectBy0 | eq ys vv2 | = |
| case | vv2 of |
|
| x | -> | if any (eq x) ys then x : [] else [] |
|
| _ | -> | [] |
|
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Case Reductions:
The following Case expression
| case | vv2 of |
| | x | → if any (eq x) ys then x : [] else [] |
| | _ | → [] |
is transformed to
| intersectBy00 | eq ys x | = if any (eq x) ys then x : [] else [] |
| intersectBy00 | eq ys _ | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
mainModule List
|
| ((intersect :: Eq a => [[a]] -> [[a]] -> [[a]]) :: Eq a => [[a]] -> [[a]] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | intersect :: Eq a => [a] -> [a] -> [a]
| intersect | | = | intersectBy (==) |
|
| | intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| intersectBy | eq xs ys | = | concatMap (intersectBy0 eq ys) xs |
|
| |
| intersectBy0 | eq ys vv2 | = | intersectBy00 eq ys vv2 |
|
| |
| intersectBy00 | eq ys x | = | if any (eq x) ys then x : [] else [] |
| intersectBy00 | eq ys _ | = | [] |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
If Reductions:
The following If expression
if any (eq x) ys then x : [] else []
is transformed to
| intersectBy000 | x True | = x : [] |
| intersectBy000 | x False | = [] |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule List
|
| ((intersect :: Eq a => [[a]] -> [[a]] -> [[a]]) :: Eq a => [[a]] -> [[a]] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | intersect :: Eq a => [a] -> [a] -> [a]
| intersect | | = | intersectBy (==) |
|
| | intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| intersectBy | eq xs ys | = | concatMap (intersectBy0 eq ys) xs |
|
| |
| intersectBy0 | eq ys vv2 | = | intersectBy00 eq ys vv2 |
|
| |
| intersectBy00 | eq ys x | = | intersectBy000 x (any (eq x) ys) |
| intersectBy00 | eq ys _ | = | [] |
|
| |
| intersectBy000 | x True | = | x : [] |
| intersectBy000 | x False | = | [] |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
|
| ((intersect :: Eq a => [[a]] -> [[a]] -> [[a]]) :: Eq a => [[a]] -> [[a]] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | intersect :: Eq a => [a] -> [a] -> [a]
| intersect | | = | intersectBy (==) |
|
| | intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| intersectBy | eq xs ys | = | concatMap (intersectBy0 eq ys) xs |
|
| |
| intersectBy0 | eq ys vv2 | = | intersectBy00 eq ys vv2 |
|
| |
| intersectBy00 | eq ys x | = | intersectBy000 x (any (eq x) ys) |
| intersectBy00 | eq ys vw | = | [] |
|
| |
| intersectBy000 | x True | = | x : [] |
| intersectBy000 | x False | = | [] |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
| undefined0 | True | = undefined |
| undefined1 | | = undefined0 False |
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule List
|
| (intersect :: Eq a => [[a]] -> [[a]] -> [[a]]) |
module List where
| | import qualified Maybe
import qualified Prelude
|
| | intersect :: Eq a => [a] -> [a] -> [a]
| intersect | | = | intersectBy (==) |
|
| | intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
| intersectBy | eq xs ys | = | concatMap (intersectBy0 eq ys) xs |
|
| |
| intersectBy0 | eq ys vv2 | = | intersectBy00 eq ys vv2 |
|
| |
| intersectBy00 | eq ys x | = | intersectBy000 x (any (eq x) ys) |
| intersectBy00 | eq ys vw | = | [] |
|
| |
| intersectBy000 | x True | = | x : [] |
| intersectBy000 | x False | = | [] |
|
module Maybe where
| | import qualified List
import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xx3300), Succ(xx4000000)) → new_primPlusNat(xx3300, xx4000000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xx3300), Succ(xx4000000)) → new_primPlusNat(xx3300, xx4000000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xx300000), Succ(xx400000)) → new_primMulNat(xx300000, Succ(xx400000))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xx300000), Succ(xx400000)) → new_primMulNat(xx300000, Succ(xx400000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xx30000), Succ(xx40000)) → new_primEqNat(xx30000, xx40000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xx30000), Succ(xx40000)) → new_primEqNat(xx30000, xx40000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, bd, app(ty_[], ec)) → new_esEs1(xx3002, xx4002, ec)
new_esEs2(Left(xx3000), Left(xx4000), app(app(ty_@2, hh), baa), ge) → new_esEs3(xx3000, xx4000, hh, baa)
new_esEs2(Left(xx3000), Left(xx4000), app(ty_[], he), ge) → new_esEs1(xx3000, xx4000, he)
new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(app(ty_@3, bbc), bbd), bbe), gg) → new_esEs(xx3000, xx4000, bbc, bbd, bbe)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(ty_Maybe, bf), bd, be) → new_esEs0(xx3000, xx4000, bf)
new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), gh) → new_esEs1(xx3011, xx4011, gh)
new_esEs0(Just(xx3000), Just(xx4000), app(ty_Maybe, fc)) → new_esEs0(xx3000, xx4000, fc)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, app(ty_[], db), be) → new_esEs1(xx3001, xx4001, db)
new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), app(ty_[], gc)) → new_esEs1(xx3010, xx4010, gc)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(app(ty_@3, ba), bb), bc), bd, be) → new_esEs(xx3000, xx4000, ba, bb, bc)
new_esEs2(Left(xx3000), Left(xx4000), app(app(ty_Either, hf), hg), ge) → new_esEs2(xx3000, xx4000, hf, hg)
new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), gf, app(ty_[], bch)) → new_esEs1(xx3001, xx4001, bch)
new_esEs2(Right(xx3000), Right(xx4000), gd, app(app(ty_@2, bba), bbb)) → new_esEs3(xx3000, xx4000, bba, bbb)
new_esEs2(Left(xx3000), Left(xx4000), app(app(app(ty_@3, ha), hb), hc), ge) → new_esEs(xx3000, xx4000, ha, hb, hc)
new_esEs2(Right(xx3000), Right(xx4000), gd, app(app(app(ty_@3, bab), bac), bad)) → new_esEs(xx3000, xx4000, bab, bac, bad)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, app(app(ty_Either, dc), dd), be) → new_esEs2(xx3001, xx4001, dc, dd)
new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), app(app(ty_Either, gd), ge)) → new_esEs2(xx3010, xx4010, gd, ge)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, bd, app(app(ty_@2, ef), eg)) → new_esEs3(xx3002, xx4002, ef, eg)
new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), app(ty_[], bbg), gg) → new_esEs1(xx3000, xx4000, bbg)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(ty_[], bg), bd, be) → new_esEs1(xx3000, xx4000, bg)
new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), gf, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs(xx3001, xx4001, bcd, bce, bcf)
new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), gf, app(app(ty_@2, bdc), bdd)) → new_esEs3(xx3001, xx4001, bdc, bdd)
new_esEs2(Right(xx3000), Right(xx4000), gd, app(ty_[], baf)) → new_esEs1(xx3000, xx4000, baf)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, app(ty_Maybe, da), be) → new_esEs0(xx3001, xx4001, da)
new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), app(app(ty_@2, gf), gg)) → new_esEs3(xx3010, xx4010, gf, gg)
new_esEs0(Just(xx3000), Just(xx4000), app(ty_[], fd)) → new_esEs1(xx3000, xx4000, fd)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(ty_@2, cb), cc), bd, be) → new_esEs3(xx3000, xx4000, cb, cc)
new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), app(ty_Maybe, bbf), gg) → new_esEs0(xx3000, xx4000, bbf)
new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), app(ty_Maybe, gb)) → new_esEs0(xx3010, xx4010, gb)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, bd, app(app(ty_Either, ed), ee)) → new_esEs2(xx3002, xx4002, ed, ee)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, app(app(app(ty_@3, ce), cf), cg), be) → new_esEs(xx3001, xx4001, ce, cf, cg)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, bd, app(ty_Maybe, eb)) → new_esEs0(xx3002, xx4002, eb)
new_esEs0(Just(xx3000), Just(xx4000), app(app(app(ty_@3, eh), fa), fb)) → new_esEs(xx3000, xx4000, eh, fa, fb)
new_esEs2(Right(xx3000), Right(xx4000), gd, app(app(ty_Either, bag), bah)) → new_esEs2(xx3000, xx4000, bag, bah)
new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(ty_@2, bcb), bcc), gg) → new_esEs3(xx3000, xx4000, bcb, bcc)
new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), app(app(app(ty_@3, cd), bd), be)) → new_esEs(xx3010, xx4010, cd, bd, be)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(ty_Either, bh), ca), bd, be) → new_esEs2(xx3000, xx4000, bh, ca)
new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), gf, app(ty_Maybe, bcg)) → new_esEs0(xx3001, xx4001, bcg)
new_esEs2(Left(xx3000), Left(xx4000), app(ty_Maybe, hd), ge) → new_esEs0(xx3000, xx4000, hd)
new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(ty_Either, bbh), bca), gg) → new_esEs2(xx3000, xx4000, bbh, bca)
new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), gf, app(app(ty_Either, bda), bdb)) → new_esEs2(xx3001, xx4001, bda, bdb)
new_esEs2(Right(xx3000), Right(xx4000), gd, app(ty_Maybe, bae)) → new_esEs0(xx3000, xx4000, bae)
new_esEs0(Just(xx3000), Just(xx4000), app(app(ty_@2, fh), ga)) → new_esEs3(xx3000, xx4000, fh, ga)
new_esEs0(Just(xx3000), Just(xx4000), app(app(ty_Either, ff), fg)) → new_esEs2(xx3000, xx4000, ff, fg)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, app(app(ty_@2, de), df), be) → new_esEs3(xx3001, xx4001, de, df)
new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, bd, app(app(app(ty_@3, dg), dh), ea)) → new_esEs(xx3002, xx4002, dg, dh, ea)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), app(app(app(ty_@3, cd), bd), be)) → new_esEs(xx3010, xx4010, cd, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), app(app(ty_Either, gd), ge)) → new_esEs2(xx3010, xx4010, gd, ge)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), app(app(ty_@2, gf), gg)) → new_esEs3(xx3010, xx4010, gf, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xx3000), Just(xx4000), app(app(app(ty_@3, eh), fa), fb)) → new_esEs(xx3000, xx4000, eh, fa, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Just(xx3000), Just(xx4000), app(app(ty_Either, ff), fg)) → new_esEs2(xx3000, xx4000, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Just(xx3000), Just(xx4000), app(app(ty_@2, fh), ga)) → new_esEs3(xx3000, xx4000, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), app(ty_Maybe, gb)) → new_esEs0(xx3010, xx4010, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(xx3000), Just(xx4000), app(ty_[], fd)) → new_esEs1(xx3000, xx4000, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Just(xx3000), Just(xx4000), app(ty_Maybe, fc)) → new_esEs0(xx3000, xx4000, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), gh) → new_esEs1(xx3011, xx4011, gh)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs1(:(xx3010, xx3011), :(xx4010, xx4011), app(ty_[], gc)) → new_esEs1(xx3010, xx4010, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(app(ty_@3, bbc), bbd), bbe), gg) → new_esEs(xx3000, xx4000, bbc, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), gf, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs(xx3001, xx4001, bcd, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(app(ty_@3, ba), bb), bc), bd, be) → new_esEs(xx3000, xx4000, ba, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, app(app(app(ty_@3, ce), cf), cg), be) → new_esEs(xx3001, xx4001, ce, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, bd, app(app(app(ty_@3, dg), dh), ea)) → new_esEs(xx3002, xx4002, dg, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs2(Left(xx3000), Left(xx4000), app(app(app(ty_@3, ha), hb), hc), ge) → new_esEs(xx3000, xx4000, ha, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Right(xx3000), Right(xx4000), gd, app(app(app(ty_@3, bab), bac), bad)) → new_esEs(xx3000, xx4000, bab, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), gf, app(app(ty_Either, bda), bdb)) → new_esEs2(xx3001, xx4001, bda, bdb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(ty_Either, bbh), bca), gg) → new_esEs2(xx3000, xx4000, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), gf, app(app(ty_@2, bdc), bdd)) → new_esEs3(xx3001, xx4001, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(ty_@2, bcb), bcc), gg) → new_esEs3(xx3000, xx4000, bcb, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), gf, app(ty_[], bch)) → new_esEs1(xx3001, xx4001, bch)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), app(ty_[], bbg), gg) → new_esEs1(xx3000, xx4000, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), app(ty_Maybe, bbf), gg) → new_esEs0(xx3000, xx4000, bbf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(xx3000, xx3001), @2(xx4000, xx4001), gf, app(ty_Maybe, bcg)) → new_esEs0(xx3001, xx4001, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, app(app(ty_Either, dc), dd), be) → new_esEs2(xx3001, xx4001, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, bd, app(app(ty_Either, ed), ee)) → new_esEs2(xx3002, xx4002, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(ty_Either, bh), ca), bd, be) → new_esEs2(xx3000, xx4000, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(xx3000), Left(xx4000), app(app(ty_Either, hf), hg), ge) → new_esEs2(xx3000, xx4000, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xx3000), Right(xx4000), gd, app(app(ty_Either, bag), bah)) → new_esEs2(xx3000, xx4000, bag, bah)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, bd, app(app(ty_@2, ef), eg)) → new_esEs3(xx3002, xx4002, ef, eg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(ty_@2, cb), cc), bd, be) → new_esEs3(xx3000, xx4000, cb, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, app(app(ty_@2, de), df), be) → new_esEs3(xx3001, xx4001, de, df)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, bd, app(ty_[], ec)) → new_esEs1(xx3002, xx4002, ec)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, app(ty_[], db), be) → new_esEs1(xx3001, xx4001, db)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(ty_[], bg), bd, be) → new_esEs1(xx3000, xx4000, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(ty_Maybe, bf), bd, be) → new_esEs0(xx3000, xx4000, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, app(ty_Maybe, da), be) → new_esEs0(xx3001, xx4001, da)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), cd, bd, app(ty_Maybe, eb)) → new_esEs0(xx3002, xx4002, eb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs2(Left(xx3000), Left(xx4000), app(app(ty_@2, hh), baa), ge) → new_esEs3(xx3000, xx4000, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xx3000), Right(xx4000), gd, app(app(ty_@2, bba), bbb)) → new_esEs3(xx3000, xx4000, bba, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(xx3000), Left(xx4000), app(ty_[], he), ge) → new_esEs1(xx3000, xx4000, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xx3000), Right(xx4000), gd, app(ty_[], baf)) → new_esEs1(xx3000, xx4000, baf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(xx3000), Left(xx4000), app(ty_Maybe, hd), ge) → new_esEs0(xx3000, xx4000, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xx3000), Right(xx4000), gd, app(ty_Maybe, bae)) → new_esEs0(xx3000, xx4000, bae)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs0(:(xx300, xx301), :([], xx41), xx5, bb) → new_psPs(xx300, xx301, False, xx41, xx5, bb)
new_psPs0(:(xx300, xx301), :(:(xx400, xx401), xx41), xx5, bb) → new_psPs(xx300, xx301, new_asAs(new_esEs4(xx300, xx400, bb), new_esEs5(xx301, xx401, bb)), xx41, xx5, bb)
new_psPs(xx13, xx14, False, xx17, xx18, ba) → new_psPs0(:(xx13, xx14), xx17, xx18, ba)
new_psPs0([], :(:(xx400, xx401), xx41), xx5, bb) → new_psPs0([], xx41, xx5, bb)
The TRS R consists of the following rules:
new_esEs25(xx3000, xx4000, ty_Ordering) → new_esEs17(xx3000, xx4000)
new_esEs14(Just(xx3000), Just(xx4000), ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Double, ca) → new_esEs8(xx3000, xx4000)
new_esEs25(xx3000, xx4000, app(ty_Maybe, bcf)) → new_esEs14(xx3000, xx4000, bcf)
new_primPlusNat1(Succ(xx3300), Succ(xx4000000)) → Succ(Succ(new_primPlusNat1(xx3300, xx4000000)))
new_primEqInt(Pos(Succ(xx30000)), Neg(xx4000)) → False
new_primEqInt(Neg(Succ(xx30000)), Pos(xx4000)) → False
new_esEs23(xx3001, xx4001, app(app(ty_@2, baf), bag)) → new_esEs18(xx3001, xx4001, baf, bag)
new_esEs4(xx300, xx400, ty_Bool) → new_esEs12(xx300, xx400)
new_esEs7(Char(xx3000), Char(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Bool, ca) → new_esEs12(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), app(ty_Maybe, da), ca) → new_esEs14(xx3000, xx4000, da)
new_esEs26(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_primEqInt(Pos(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xx40000))) → False
new_esEs16(Left(xx3000), Left(xx4000), app(ty_Ratio, dg), ca) → new_esEs19(xx3000, xx4000, dg)
new_esEs4(xx300, xx400, app(app(app(ty_@3, bc), bd), be)) → new_esEs13(xx300, xx400, bc, bd, be)
new_esEs5([], [], bb) → True
new_esEs11(xx3010, xx4010, app(ty_[], bg)) → new_esEs5(xx3010, xx4010, bg)
new_esEs20(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs14(Just(xx3000), Just(xx4000), ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs23(xx3001, xx4001, app(ty_Maybe, bab)) → new_esEs14(xx3001, xx4001, bab)
new_esEs25(xx3000, xx4000, ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_@0) → new_esEs10(xx3010, xx4010)
new_esEs22(xx3000, xx4000, ty_Integer) → new_esEs6(xx3000, xx4000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs22(xx3000, xx4000, ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3001, xx4001, ty_Float) → new_esEs15(xx3001, xx4001)
new_esEs4(xx300, xx400, ty_@0) → new_esEs10(xx300, xx400)
new_esEs12(True, True) → True
new_esEs5([], :(xx4010, xx4011), bb) → False
new_esEs5(:(xx3010, xx3011), [], bb) → False
new_esEs25(xx3000, xx4000, ty_Double) → new_esEs8(xx3000, xx4000)
new_primPlusNat0(Zero, xx400000) → Succ(xx400000)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs6(Integer(xx3000), Integer(xx4000)) → new_primEqInt(xx3000, xx4000)
new_esEs23(xx3001, xx4001, ty_Bool) → new_esEs12(xx3001, xx4001)
new_esEs4(xx300, xx400, ty_Float) → new_esEs15(xx300, xx400)
new_sr(Pos(xx30000), Neg(xx40000)) → Neg(new_primMulNat0(xx30000, xx40000))
new_sr(Neg(xx30000), Pos(xx40000)) → Neg(new_primMulNat0(xx30000, xx40000))
new_esEs23(xx3001, xx4001, ty_@0) → new_esEs10(xx3001, xx4001)
new_esEs14(Just(xx3000), Just(xx4000), ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs22(xx3000, xx4000, app(ty_Ratio, hf)) → new_esEs19(xx3000, xx4000, hf)
new_esEs15(Float(xx3000, xx3001), Float(xx4000, xx4001)) → new_esEs9(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs16(Right(xx3000), Right(xx4000), bh, app(app(ty_Either, ee), ef)) → new_esEs16(xx3000, xx4000, ee, ef)
new_esEs24(xx3002, xx4002, ty_Char) → new_esEs7(xx3002, xx4002)
new_esEs26(xx3001, xx4001, ty_Double) → new_esEs8(xx3001, xx4001)
new_esEs16(Left(xx3000), Left(xx4000), ty_Int, ca) → new_esEs9(xx3000, xx4000)
new_esEs18(@2(xx3000, xx3001), @2(xx4000, xx4001), cb, cc) → new_asAs(new_esEs25(xx3000, xx4000, cb), new_esEs26(xx3001, xx4001, cc))
new_esEs11(xx3010, xx4010, app(app(ty_Either, bh), ca)) → new_esEs16(xx3010, xx4010, bh, ca)
new_esEs26(xx3001, xx4001, app(app(ty_@2, bed), bee)) → new_esEs18(xx3001, xx4001, bed, bee)
new_esEs26(xx3001, xx4001, ty_@0) → new_esEs10(xx3001, xx4001)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(ty_[], ed)) → new_esEs5(xx3000, xx4000, ed)
new_esEs26(xx3001, xx4001, ty_Integer) → new_esEs6(xx3001, xx4001)
new_esEs22(xx3000, xx4000, app(app(ty_@2, hd), he)) → new_esEs18(xx3000, xx4000, hd, he)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(ty_Maybe, ec)) → new_esEs14(xx3000, xx4000, ec)
new_primEqNat0(Zero, Succ(xx40000)) → False
new_primEqNat0(Succ(xx30000), Zero) → False
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Double) → new_esEs8(xx3000, xx4000)
new_esEs21(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_esEs24(xx3002, xx4002, app(ty_Maybe, bbd)) → new_esEs14(xx3002, xx4002, bbd)
new_esEs4(xx300, xx400, app(ty_[], bg)) → new_esEs5(xx300, xx400, bg)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Ordering) → new_esEs17(xx3000, xx4000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs26(xx3001, xx4001, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs13(xx3001, xx4001, bde, bdf, bdg)
new_esEs23(xx3001, xx4001, ty_Integer) → new_esEs6(xx3001, xx4001)
new_esEs22(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Float, ca) → new_esEs15(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Bool) → new_esEs12(xx3010, xx4010)
new_esEs23(xx3001, xx4001, ty_Double) → new_esEs8(xx3001, xx4001)
new_esEs4(xx300, xx400, app(ty_Ratio, cd)) → new_esEs19(xx300, xx400, cd)
new_esEs22(xx3000, xx4000, ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), app(app(ty_Either, dc), dd), ca) → new_esEs16(xx3000, xx4000, dc, dd)
new_esEs26(xx3001, xx4001, ty_Bool) → new_esEs12(xx3001, xx4001)
new_esEs23(xx3001, xx4001, app(ty_[], bac)) → new_esEs5(xx3001, xx4001, bac)
new_esEs24(xx3002, xx4002, ty_Int) → new_esEs9(xx3002, xx4002)
new_esEs16(Left(xx3000), Right(xx4000), bh, ca) → False
new_esEs16(Right(xx3000), Left(xx4000), bh, ca) → False
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), app(ty_[], db), ca) → new_esEs5(xx3000, xx4000, db)
new_esEs19(:%(xx3000, xx3001), :%(xx4000, xx4001), cd) → new_asAs(new_esEs20(xx3000, xx4000, cd), new_esEs21(xx3001, xx4001, cd))
new_esEs25(xx3000, xx4000, ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs4(xx300, xx400, app(app(ty_@2, cb), cc)) → new_esEs18(xx300, xx400, cb, cc)
new_esEs23(xx3001, xx4001, ty_Char) → new_esEs7(xx3001, xx4001)
new_esEs22(xx3000, xx4000, ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs4(xx300, xx400, ty_Integer) → new_esEs6(xx300, xx400)
new_esEs23(xx3001, xx4001, ty_Ordering) → new_esEs17(xx3001, xx4001)
new_esEs17(LT, LT) → True
new_esEs14(Just(xx3000), Just(xx4000), app(ty_[], fg)) → new_esEs5(xx3000, xx4000, fg)
new_esEs5(:(xx3010, xx3011), :(xx4010, xx4011), bb) → new_asAs(new_esEs11(xx3010, xx4010, bb), new_esEs5(xx3011, xx4011, bb))
new_esEs22(xx3000, xx4000, app(ty_[], ha)) → new_esEs5(xx3000, xx4000, ha)
new_esEs14(Just(xx3000), Just(xx4000), app(app(ty_@2, gb), gc)) → new_esEs18(xx3000, xx4000, gb, gc)
new_esEs10(@0, @0) → True
new_esEs25(xx3000, xx4000, ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs11(xx3010, xx4010, app(app(app(ty_@3, bc), bd), be)) → new_esEs13(xx3010, xx4010, bc, bd, be)
new_sr(Neg(xx30000), Neg(xx40000)) → Pos(new_primMulNat0(xx30000, xx40000))
new_esEs14(Nothing, Nothing, bf) → True
new_asAs(False, xx32) → False
new_sr(Pos(xx30000), Pos(xx40000)) → Pos(new_primMulNat0(xx30000, xx40000))
new_esEs25(xx3000, xx4000, app(ty_[], bcg)) → new_esEs5(xx3000, xx4000, bcg)
new_esEs14(Just(xx3000), Just(xx4000), ty_Double) → new_esEs8(xx3000, xx4000)
new_primEqNat0(Zero, Zero) → True
new_esEs16(Left(xx3000), Left(xx4000), ty_Integer, ca) → new_esEs6(xx3000, xx4000)
new_primMulNat0(Zero, Succ(xx400000)) → Zero
new_primMulNat0(Succ(xx300000), Zero) → Zero
new_esEs14(Just(xx3000), Just(xx4000), ty_Ordering) → new_esEs17(xx3000, xx4000)
new_esEs25(xx3000, xx4000, ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs23(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_esEs23(xx3001, xx4001, app(app(app(ty_@3, hg), hh), baa)) → new_esEs13(xx3001, xx4001, hg, hh, baa)
new_esEs22(xx3000, xx4000, app(app(ty_Either, hb), hc)) → new_esEs16(xx3000, xx4000, hb, hc)
new_esEs22(xx3000, xx4000, app(app(app(ty_@3, ge), gf), gg)) → new_esEs13(xx3000, xx4000, ge, gf, gg)
new_esEs16(Left(xx3000), Left(xx4000), ty_Ordering, ca) → new_esEs17(xx3000, xx4000)
new_esEs23(xx3001, xx4001, ty_Float) → new_esEs15(xx3001, xx4001)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs14(Just(xx3000), Just(xx4000), ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3001, xx4001, ty_Char) → new_esEs7(xx3001, xx4001)
new_esEs26(xx3001, xx4001, app(app(ty_Either, beb), bec)) → new_esEs16(xx3001, xx4001, beb, bec)
new_esEs14(Just(xx3000), Just(xx4000), app(ty_Maybe, ff)) → new_esEs14(xx3000, xx4000, ff)
new_esEs11(xx3010, xx4010, ty_Double) → new_esEs8(xx3010, xx4010)
new_esEs24(xx3002, xx4002, ty_Bool) → new_esEs12(xx3002, xx4002)
new_esEs23(xx3001, xx4001, app(ty_Ratio, bah)) → new_esEs19(xx3001, xx4001, bah)
new_esEs24(xx3002, xx4002, app(ty_[], bbe)) → new_esEs5(xx3002, xx4002, bbe)
new_esEs23(xx3001, xx4001, app(app(ty_Either, bad), bae)) → new_esEs16(xx3001, xx4001, bad, bae)
new_esEs25(xx3000, xx4000, ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs26(xx3001, xx4001, app(ty_[], bea)) → new_esEs5(xx3001, xx4001, bea)
new_esEs11(xx3010, xx4010, app(ty_Ratio, cd)) → new_esEs19(xx3010, xx4010, cd)
new_primPlusNat0(Succ(xx330), xx400000) → Succ(Succ(new_primPlusNat1(xx330, xx400000)))
new_esEs17(LT, EQ) → False
new_esEs14(Just(xx3000), Just(xx4000), app(app(ty_Either, fh), ga)) → new_esEs16(xx3000, xx4000, fh, ga)
new_esEs17(EQ, LT) → False
new_esEs12(False, False) → True
new_esEs12(False, True) → False
new_esEs12(True, False) → False
new_esEs25(xx3000, xx4000, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs13(xx3000, xx4000, bcc, bcd, bce)
new_esEs14(Just(xx3000), Just(xx4000), app(app(app(ty_@3, fb), fc), fd)) → new_esEs13(xx3000, xx4000, fb, fc, fd)
new_esEs14(Just(xx3000), Nothing, bf) → False
new_esEs14(Nothing, Just(xx4000), bf) → False
new_primEqInt(Neg(Succ(xx30000)), Neg(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs24(xx3002, xx4002, ty_Double) → new_esEs8(xx3002, xx4002)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(app(ty_@2, eg), eh)) → new_esEs18(xx3000, xx4000, eg, eh)
new_esEs4(xx300, xx400, ty_Char) → new_esEs7(xx300, xx400)
new_esEs14(Just(xx3000), Just(xx4000), ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs25(xx3000, xx4000, app(app(ty_@2, bdb), bdc)) → new_esEs18(xx3000, xx4000, bdb, bdc)
new_esEs24(xx3002, xx4002, app(app(ty_@2, bbh), bca)) → new_esEs18(xx3002, xx4002, bbh, bca)
new_esEs24(xx3002, xx4002, ty_Ordering) → new_esEs17(xx3002, xx4002)
new_esEs4(xx300, xx400, ty_Double) → new_esEs8(xx300, xx400)
new_primPlusNat1(Succ(xx3300), Zero) → Succ(xx3300)
new_primPlusNat1(Zero, Succ(xx4000000)) → Succ(xx4000000)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(ty_Ratio, fa)) → new_esEs19(xx3000, xx4000, fa)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs8(Double(xx3000, xx3001), Double(xx4000, xx4001)) → new_esEs9(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs26(xx3001, xx4001, ty_Ordering) → new_esEs17(xx3001, xx4001)
new_esEs16(Left(xx3000), Left(xx4000), ty_@0, ca) → new_esEs10(xx3000, xx4000)
new_esEs22(xx3000, xx4000, ty_Ordering) → new_esEs17(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Int) → new_esEs9(xx3010, xx4010)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs14(Just(xx3000), Just(xx4000), app(ty_Ratio, gd)) → new_esEs19(xx3000, xx4000, gd)
new_esEs17(EQ, EQ) → True
new_esEs4(xx300, xx400, app(app(ty_Either, bh), ca)) → new_esEs16(xx300, xx400, bh, ca)
new_esEs24(xx3002, xx4002, app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs13(xx3002, xx4002, bba, bbb, bbc)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs26(xx3001, xx4001, app(ty_Maybe, bdh)) → new_esEs14(xx3001, xx4001, bdh)
new_esEs11(xx3010, xx4010, ty_Float) → new_esEs15(xx3010, xx4010)
new_primEqInt(Neg(Succ(xx30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xx40000))) → False
new_esEs16(Right(xx3000), Right(xx4000), bh, app(app(app(ty_@3, dh), ea), eb)) → new_esEs13(xx3000, xx4000, dh, ea, eb)
new_esEs20(xx3000, xx4000, ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs21(xx3001, xx4001, ty_Integer) → new_esEs6(xx3001, xx4001)
new_esEs22(xx3000, xx4000, app(ty_Maybe, gh)) → new_esEs14(xx3000, xx4000, gh)
new_esEs25(xx3000, xx4000, app(ty_Ratio, bdd)) → new_esEs19(xx3000, xx4000, bdd)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs16(Left(xx3000), Left(xx4000), app(app(app(ty_@3, ce), cf), cg), ca) → new_esEs13(xx3000, xx4000, ce, cf, cg)
new_asAs(True, xx32) → xx32
new_esEs16(Left(xx3000), Left(xx4000), app(app(ty_@2, de), df), ca) → new_esEs18(xx3000, xx4000, de, df)
new_primMulNat0(Succ(xx300000), Succ(xx400000)) → new_primPlusNat0(new_primMulNat0(xx300000, Succ(xx400000)), xx400000)
new_esEs17(GT, GT) → True
new_esEs22(xx3000, xx4000, ty_Double) → new_esEs8(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Integer) → new_esEs6(xx3010, xx4010)
new_primEqInt(Pos(Succ(xx30000)), Pos(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Char, ca) → new_esEs7(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Ordering) → new_esEs17(xx3010, xx4010)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs25(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs17(LT, GT) → False
new_esEs17(GT, LT) → False
new_esEs11(xx3010, xx4010, app(app(ty_@2, cb), cc)) → new_esEs18(xx3010, xx4010, cb, cc)
new_esEs24(xx3002, xx4002, app(app(ty_Either, bbf), bbg)) → new_esEs16(xx3002, xx4002, bbf, bbg)
new_primEqNat0(Succ(xx30000), Succ(xx40000)) → new_primEqNat0(xx30000, xx40000)
new_esEs17(EQ, GT) → False
new_esEs17(GT, EQ) → False
new_esEs9(xx300, xx400) → new_primEqInt(xx300, xx400)
new_esEs26(xx3001, xx4001, app(ty_Ratio, bef)) → new_esEs19(xx3001, xx4001, bef)
new_esEs14(Just(xx3000), Just(xx4000), ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs4(xx300, xx400, app(ty_Maybe, bf)) → new_esEs14(xx300, xx400, bf)
new_esEs25(xx3000, xx4000, app(app(ty_Either, bch), bda)) → new_esEs16(xx3000, xx4000, bch, bda)
new_esEs22(xx3000, xx4000, ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs24(xx3002, xx4002, ty_Integer) → new_esEs6(xx3002, xx4002)
new_esEs4(xx300, xx400, ty_Int) → new_esEs9(xx300, xx400)
new_esEs11(xx3010, xx4010, app(ty_Maybe, bf)) → new_esEs14(xx3010, xx4010, bf)
new_esEs4(xx300, xx400, ty_Ordering) → new_esEs17(xx300, xx400)
new_primEqInt(Pos(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs13(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), bc, bd, be) → new_asAs(new_esEs22(xx3000, xx4000, bc), new_asAs(new_esEs23(xx3001, xx4001, bd), new_esEs24(xx3002, xx4002, be)))
new_esEs24(xx3002, xx4002, ty_Float) → new_esEs15(xx3002, xx4002)
new_esEs11(xx3010, xx4010, ty_Char) → new_esEs7(xx3010, xx4010)
new_esEs24(xx3002, xx4002, ty_@0) → new_esEs10(xx3002, xx4002)
new_esEs24(xx3002, xx4002, app(ty_Ratio, bcb)) → new_esEs19(xx3002, xx4002, bcb)
The set Q consists of the following terms:
new_esEs10(@0, @0)
new_esEs17(GT, LT)
new_esEs17(LT, GT)
new_esEs14(Just(x0), Just(x1), app(ty_[], x2))
new_esEs12(True, True)
new_esEs11(x0, x1, ty_Int)
new_esEs9(x0, x1)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Char)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs5([], [], x0)
new_esEs4(x0, x1, ty_Double)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Double)
new_esEs16(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Right(x0), Right(x1), x2, ty_Float)
new_esEs17(LT, LT)
new_esEs5([], :(x0, x1), x2)
new_esEs16(Left(x0), Left(x1), ty_@0, x2)
new_esEs25(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs24(x0, x1, ty_Bool)
new_esEs12(False, False)
new_primEqNat0(Succ(x0), Zero)
new_esEs14(Just(x0), Just(x1), ty_Ordering)
new_esEs7(Char(x0), Char(x1))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Float)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(x0, x1, ty_Float)
new_esEs16(Left(x0), Left(x1), ty_Double, x2)
new_esEs14(Just(x0), Just(x1), ty_Char)
new_esEs16(Left(x0), Left(x1), ty_Int, x2)
new_esEs26(x0, x1, ty_@0)
new_esEs11(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Char, x2)
new_esEs25(x0, x1, ty_Int)
new_esEs14(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(GT, EQ)
new_esEs17(EQ, GT)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs24(x0, x1, ty_Double)
new_esEs16(Right(x0), Right(x1), x2, ty_Integer)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs14(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs11(x0, x1, ty_Double)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primPlusNat1(Succ(x0), Zero)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_primPlusNat0(Succ(x0), x1)
new_esEs14(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Float)
new_esEs17(GT, GT)
new_esEs4(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, ty_Float)
new_esEs14(Just(x0), Just(x1), ty_Double)
new_esEs16(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs16(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Zero, Zero)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs4(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs16(Left(x0), Right(x1), x2, x3)
new_esEs16(Right(x0), Left(x1), x2, x3)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs14(Just(x0), Just(x1), ty_Float)
new_esEs24(x0, x1, ty_@0)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_@0)
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs11(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs14(Just(x0), Just(x1), ty_Int)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Zero)
new_esEs12(True, False)
new_esEs12(False, True)
new_esEs21(x0, x1, ty_Int)
new_esEs16(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs16(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs23(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs14(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Double)
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_esEs14(Nothing, Nothing, x0)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs25(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Right(x0), Right(x1), x2, ty_Bool)
new_esEs16(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs22(x0, x1, ty_@0)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Float)
new_esEs19(:%(x0, x1), :%(x2, x3), x4)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs14(Just(x0), Nothing, x1)
new_esEs24(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Float, x2)
new_esEs16(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs24(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, ty_Ordering)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqNat0(Zero, Succ(x0))
new_esEs5(:(x0, x1), [], x2)
new_esEs14(Just(x0), Just(x1), ty_@0)
new_esEs11(x0, x1, ty_@0)
new_esEs14(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat1(Zero, Zero)
new_esEs25(x0, x1, ty_Char)
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs14(Just(x0), Just(x1), ty_Integer)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs16(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs26(x0, x1, app(ty_[], x2))
new_asAs(True, x0)
new_esEs11(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Int)
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs16(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs4(x0, x1, ty_Float)
new_esEs17(EQ, EQ)
new_esEs14(Nothing, Just(x0), x1)
new_esEs6(Integer(x0), Integer(x1))
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Bool)
new_esEs14(Just(x0), Just(x1), ty_Bool)
new_esEs25(x0, x1, ty_Bool)
new_asAs(False, x0)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Integer)
new_esEs16(Right(x0), Right(x1), x2, ty_Int)
new_esEs23(x0, x1, ty_Double)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs0([], :(:(xx400, xx401), xx41), xx5, bb) → new_psPs0([], xx41, xx5, bb)
The TRS R consists of the following rules:
new_esEs25(xx3000, xx4000, ty_Ordering) → new_esEs17(xx3000, xx4000)
new_esEs14(Just(xx3000), Just(xx4000), ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Double, ca) → new_esEs8(xx3000, xx4000)
new_esEs25(xx3000, xx4000, app(ty_Maybe, bcf)) → new_esEs14(xx3000, xx4000, bcf)
new_primPlusNat1(Succ(xx3300), Succ(xx4000000)) → Succ(Succ(new_primPlusNat1(xx3300, xx4000000)))
new_primEqInt(Pos(Succ(xx30000)), Neg(xx4000)) → False
new_primEqInt(Neg(Succ(xx30000)), Pos(xx4000)) → False
new_esEs23(xx3001, xx4001, app(app(ty_@2, baf), bag)) → new_esEs18(xx3001, xx4001, baf, bag)
new_esEs4(xx300, xx400, ty_Bool) → new_esEs12(xx300, xx400)
new_esEs7(Char(xx3000), Char(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Bool, ca) → new_esEs12(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), app(ty_Maybe, da), ca) → new_esEs14(xx3000, xx4000, da)
new_esEs26(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_primEqInt(Pos(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xx40000))) → False
new_esEs16(Left(xx3000), Left(xx4000), app(ty_Ratio, dg), ca) → new_esEs19(xx3000, xx4000, dg)
new_esEs4(xx300, xx400, app(app(app(ty_@3, bc), bd), be)) → new_esEs13(xx300, xx400, bc, bd, be)
new_esEs5([], [], bb) → True
new_esEs11(xx3010, xx4010, app(ty_[], bg)) → new_esEs5(xx3010, xx4010, bg)
new_esEs20(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs14(Just(xx3000), Just(xx4000), ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs23(xx3001, xx4001, app(ty_Maybe, bab)) → new_esEs14(xx3001, xx4001, bab)
new_esEs25(xx3000, xx4000, ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_@0) → new_esEs10(xx3010, xx4010)
new_esEs22(xx3000, xx4000, ty_Integer) → new_esEs6(xx3000, xx4000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs22(xx3000, xx4000, ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3001, xx4001, ty_Float) → new_esEs15(xx3001, xx4001)
new_esEs4(xx300, xx400, ty_@0) → new_esEs10(xx300, xx400)
new_esEs12(True, True) → True
new_esEs5([], :(xx4010, xx4011), bb) → False
new_esEs5(:(xx3010, xx3011), [], bb) → False
new_esEs25(xx3000, xx4000, ty_Double) → new_esEs8(xx3000, xx4000)
new_primPlusNat0(Zero, xx400000) → Succ(xx400000)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs6(Integer(xx3000), Integer(xx4000)) → new_primEqInt(xx3000, xx4000)
new_esEs23(xx3001, xx4001, ty_Bool) → new_esEs12(xx3001, xx4001)
new_esEs4(xx300, xx400, ty_Float) → new_esEs15(xx300, xx400)
new_sr(Pos(xx30000), Neg(xx40000)) → Neg(new_primMulNat0(xx30000, xx40000))
new_sr(Neg(xx30000), Pos(xx40000)) → Neg(new_primMulNat0(xx30000, xx40000))
new_esEs23(xx3001, xx4001, ty_@0) → new_esEs10(xx3001, xx4001)
new_esEs14(Just(xx3000), Just(xx4000), ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs22(xx3000, xx4000, app(ty_Ratio, hf)) → new_esEs19(xx3000, xx4000, hf)
new_esEs15(Float(xx3000, xx3001), Float(xx4000, xx4001)) → new_esEs9(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs16(Right(xx3000), Right(xx4000), bh, app(app(ty_Either, ee), ef)) → new_esEs16(xx3000, xx4000, ee, ef)
new_esEs24(xx3002, xx4002, ty_Char) → new_esEs7(xx3002, xx4002)
new_esEs26(xx3001, xx4001, ty_Double) → new_esEs8(xx3001, xx4001)
new_esEs16(Left(xx3000), Left(xx4000), ty_Int, ca) → new_esEs9(xx3000, xx4000)
new_esEs18(@2(xx3000, xx3001), @2(xx4000, xx4001), cb, cc) → new_asAs(new_esEs25(xx3000, xx4000, cb), new_esEs26(xx3001, xx4001, cc))
new_esEs11(xx3010, xx4010, app(app(ty_Either, bh), ca)) → new_esEs16(xx3010, xx4010, bh, ca)
new_esEs26(xx3001, xx4001, app(app(ty_@2, bed), bee)) → new_esEs18(xx3001, xx4001, bed, bee)
new_esEs26(xx3001, xx4001, ty_@0) → new_esEs10(xx3001, xx4001)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(ty_[], ed)) → new_esEs5(xx3000, xx4000, ed)
new_esEs26(xx3001, xx4001, ty_Integer) → new_esEs6(xx3001, xx4001)
new_esEs22(xx3000, xx4000, app(app(ty_@2, hd), he)) → new_esEs18(xx3000, xx4000, hd, he)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(ty_Maybe, ec)) → new_esEs14(xx3000, xx4000, ec)
new_primEqNat0(Zero, Succ(xx40000)) → False
new_primEqNat0(Succ(xx30000), Zero) → False
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Double) → new_esEs8(xx3000, xx4000)
new_esEs21(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_esEs24(xx3002, xx4002, app(ty_Maybe, bbd)) → new_esEs14(xx3002, xx4002, bbd)
new_esEs4(xx300, xx400, app(ty_[], bg)) → new_esEs5(xx300, xx400, bg)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Ordering) → new_esEs17(xx3000, xx4000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs26(xx3001, xx4001, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs13(xx3001, xx4001, bde, bdf, bdg)
new_esEs23(xx3001, xx4001, ty_Integer) → new_esEs6(xx3001, xx4001)
new_esEs22(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Float, ca) → new_esEs15(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Bool) → new_esEs12(xx3010, xx4010)
new_esEs23(xx3001, xx4001, ty_Double) → new_esEs8(xx3001, xx4001)
new_esEs4(xx300, xx400, app(ty_Ratio, cd)) → new_esEs19(xx300, xx400, cd)
new_esEs22(xx3000, xx4000, ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), app(app(ty_Either, dc), dd), ca) → new_esEs16(xx3000, xx4000, dc, dd)
new_esEs26(xx3001, xx4001, ty_Bool) → new_esEs12(xx3001, xx4001)
new_esEs23(xx3001, xx4001, app(ty_[], bac)) → new_esEs5(xx3001, xx4001, bac)
new_esEs24(xx3002, xx4002, ty_Int) → new_esEs9(xx3002, xx4002)
new_esEs16(Left(xx3000), Right(xx4000), bh, ca) → False
new_esEs16(Right(xx3000), Left(xx4000), bh, ca) → False
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), app(ty_[], db), ca) → new_esEs5(xx3000, xx4000, db)
new_esEs19(:%(xx3000, xx3001), :%(xx4000, xx4001), cd) → new_asAs(new_esEs20(xx3000, xx4000, cd), new_esEs21(xx3001, xx4001, cd))
new_esEs25(xx3000, xx4000, ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs4(xx300, xx400, app(app(ty_@2, cb), cc)) → new_esEs18(xx300, xx400, cb, cc)
new_esEs23(xx3001, xx4001, ty_Char) → new_esEs7(xx3001, xx4001)
new_esEs22(xx3000, xx4000, ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs4(xx300, xx400, ty_Integer) → new_esEs6(xx300, xx400)
new_esEs23(xx3001, xx4001, ty_Ordering) → new_esEs17(xx3001, xx4001)
new_esEs17(LT, LT) → True
new_esEs14(Just(xx3000), Just(xx4000), app(ty_[], fg)) → new_esEs5(xx3000, xx4000, fg)
new_esEs5(:(xx3010, xx3011), :(xx4010, xx4011), bb) → new_asAs(new_esEs11(xx3010, xx4010, bb), new_esEs5(xx3011, xx4011, bb))
new_esEs22(xx3000, xx4000, app(ty_[], ha)) → new_esEs5(xx3000, xx4000, ha)
new_esEs14(Just(xx3000), Just(xx4000), app(app(ty_@2, gb), gc)) → new_esEs18(xx3000, xx4000, gb, gc)
new_esEs10(@0, @0) → True
new_esEs25(xx3000, xx4000, ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs11(xx3010, xx4010, app(app(app(ty_@3, bc), bd), be)) → new_esEs13(xx3010, xx4010, bc, bd, be)
new_sr(Neg(xx30000), Neg(xx40000)) → Pos(new_primMulNat0(xx30000, xx40000))
new_esEs14(Nothing, Nothing, bf) → True
new_asAs(False, xx32) → False
new_sr(Pos(xx30000), Pos(xx40000)) → Pos(new_primMulNat0(xx30000, xx40000))
new_esEs25(xx3000, xx4000, app(ty_[], bcg)) → new_esEs5(xx3000, xx4000, bcg)
new_esEs14(Just(xx3000), Just(xx4000), ty_Double) → new_esEs8(xx3000, xx4000)
new_primEqNat0(Zero, Zero) → True
new_esEs16(Left(xx3000), Left(xx4000), ty_Integer, ca) → new_esEs6(xx3000, xx4000)
new_primMulNat0(Zero, Succ(xx400000)) → Zero
new_primMulNat0(Succ(xx300000), Zero) → Zero
new_esEs14(Just(xx3000), Just(xx4000), ty_Ordering) → new_esEs17(xx3000, xx4000)
new_esEs25(xx3000, xx4000, ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs23(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_esEs23(xx3001, xx4001, app(app(app(ty_@3, hg), hh), baa)) → new_esEs13(xx3001, xx4001, hg, hh, baa)
new_esEs22(xx3000, xx4000, app(app(ty_Either, hb), hc)) → new_esEs16(xx3000, xx4000, hb, hc)
new_esEs22(xx3000, xx4000, app(app(app(ty_@3, ge), gf), gg)) → new_esEs13(xx3000, xx4000, ge, gf, gg)
new_esEs16(Left(xx3000), Left(xx4000), ty_Ordering, ca) → new_esEs17(xx3000, xx4000)
new_esEs23(xx3001, xx4001, ty_Float) → new_esEs15(xx3001, xx4001)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs14(Just(xx3000), Just(xx4000), ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3001, xx4001, ty_Char) → new_esEs7(xx3001, xx4001)
new_esEs26(xx3001, xx4001, app(app(ty_Either, beb), bec)) → new_esEs16(xx3001, xx4001, beb, bec)
new_esEs14(Just(xx3000), Just(xx4000), app(ty_Maybe, ff)) → new_esEs14(xx3000, xx4000, ff)
new_esEs11(xx3010, xx4010, ty_Double) → new_esEs8(xx3010, xx4010)
new_esEs24(xx3002, xx4002, ty_Bool) → new_esEs12(xx3002, xx4002)
new_esEs23(xx3001, xx4001, app(ty_Ratio, bah)) → new_esEs19(xx3001, xx4001, bah)
new_esEs24(xx3002, xx4002, app(ty_[], bbe)) → new_esEs5(xx3002, xx4002, bbe)
new_esEs23(xx3001, xx4001, app(app(ty_Either, bad), bae)) → new_esEs16(xx3001, xx4001, bad, bae)
new_esEs25(xx3000, xx4000, ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs26(xx3001, xx4001, app(ty_[], bea)) → new_esEs5(xx3001, xx4001, bea)
new_esEs11(xx3010, xx4010, app(ty_Ratio, cd)) → new_esEs19(xx3010, xx4010, cd)
new_primPlusNat0(Succ(xx330), xx400000) → Succ(Succ(new_primPlusNat1(xx330, xx400000)))
new_esEs17(LT, EQ) → False
new_esEs14(Just(xx3000), Just(xx4000), app(app(ty_Either, fh), ga)) → new_esEs16(xx3000, xx4000, fh, ga)
new_esEs17(EQ, LT) → False
new_esEs12(False, False) → True
new_esEs12(False, True) → False
new_esEs12(True, False) → False
new_esEs25(xx3000, xx4000, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs13(xx3000, xx4000, bcc, bcd, bce)
new_esEs14(Just(xx3000), Just(xx4000), app(app(app(ty_@3, fb), fc), fd)) → new_esEs13(xx3000, xx4000, fb, fc, fd)
new_esEs14(Just(xx3000), Nothing, bf) → False
new_esEs14(Nothing, Just(xx4000), bf) → False
new_primEqInt(Neg(Succ(xx30000)), Neg(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs24(xx3002, xx4002, ty_Double) → new_esEs8(xx3002, xx4002)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(app(ty_@2, eg), eh)) → new_esEs18(xx3000, xx4000, eg, eh)
new_esEs4(xx300, xx400, ty_Char) → new_esEs7(xx300, xx400)
new_esEs14(Just(xx3000), Just(xx4000), ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs25(xx3000, xx4000, app(app(ty_@2, bdb), bdc)) → new_esEs18(xx3000, xx4000, bdb, bdc)
new_esEs24(xx3002, xx4002, app(app(ty_@2, bbh), bca)) → new_esEs18(xx3002, xx4002, bbh, bca)
new_esEs24(xx3002, xx4002, ty_Ordering) → new_esEs17(xx3002, xx4002)
new_esEs4(xx300, xx400, ty_Double) → new_esEs8(xx300, xx400)
new_primPlusNat1(Succ(xx3300), Zero) → Succ(xx3300)
new_primPlusNat1(Zero, Succ(xx4000000)) → Succ(xx4000000)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(ty_Ratio, fa)) → new_esEs19(xx3000, xx4000, fa)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs8(Double(xx3000, xx3001), Double(xx4000, xx4001)) → new_esEs9(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs26(xx3001, xx4001, ty_Ordering) → new_esEs17(xx3001, xx4001)
new_esEs16(Left(xx3000), Left(xx4000), ty_@0, ca) → new_esEs10(xx3000, xx4000)
new_esEs22(xx3000, xx4000, ty_Ordering) → new_esEs17(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Int) → new_esEs9(xx3010, xx4010)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs14(Just(xx3000), Just(xx4000), app(ty_Ratio, gd)) → new_esEs19(xx3000, xx4000, gd)
new_esEs17(EQ, EQ) → True
new_esEs4(xx300, xx400, app(app(ty_Either, bh), ca)) → new_esEs16(xx300, xx400, bh, ca)
new_esEs24(xx3002, xx4002, app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs13(xx3002, xx4002, bba, bbb, bbc)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs26(xx3001, xx4001, app(ty_Maybe, bdh)) → new_esEs14(xx3001, xx4001, bdh)
new_esEs11(xx3010, xx4010, ty_Float) → new_esEs15(xx3010, xx4010)
new_primEqInt(Neg(Succ(xx30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xx40000))) → False
new_esEs16(Right(xx3000), Right(xx4000), bh, app(app(app(ty_@3, dh), ea), eb)) → new_esEs13(xx3000, xx4000, dh, ea, eb)
new_esEs20(xx3000, xx4000, ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs21(xx3001, xx4001, ty_Integer) → new_esEs6(xx3001, xx4001)
new_esEs22(xx3000, xx4000, app(ty_Maybe, gh)) → new_esEs14(xx3000, xx4000, gh)
new_esEs25(xx3000, xx4000, app(ty_Ratio, bdd)) → new_esEs19(xx3000, xx4000, bdd)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs16(Left(xx3000), Left(xx4000), app(app(app(ty_@3, ce), cf), cg), ca) → new_esEs13(xx3000, xx4000, ce, cf, cg)
new_asAs(True, xx32) → xx32
new_esEs16(Left(xx3000), Left(xx4000), app(app(ty_@2, de), df), ca) → new_esEs18(xx3000, xx4000, de, df)
new_primMulNat0(Succ(xx300000), Succ(xx400000)) → new_primPlusNat0(new_primMulNat0(xx300000, Succ(xx400000)), xx400000)
new_esEs17(GT, GT) → True
new_esEs22(xx3000, xx4000, ty_Double) → new_esEs8(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Integer) → new_esEs6(xx3010, xx4010)
new_primEqInt(Pos(Succ(xx30000)), Pos(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Char, ca) → new_esEs7(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Ordering) → new_esEs17(xx3010, xx4010)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs25(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs17(LT, GT) → False
new_esEs17(GT, LT) → False
new_esEs11(xx3010, xx4010, app(app(ty_@2, cb), cc)) → new_esEs18(xx3010, xx4010, cb, cc)
new_esEs24(xx3002, xx4002, app(app(ty_Either, bbf), bbg)) → new_esEs16(xx3002, xx4002, bbf, bbg)
new_primEqNat0(Succ(xx30000), Succ(xx40000)) → new_primEqNat0(xx30000, xx40000)
new_esEs17(EQ, GT) → False
new_esEs17(GT, EQ) → False
new_esEs9(xx300, xx400) → new_primEqInt(xx300, xx400)
new_esEs26(xx3001, xx4001, app(ty_Ratio, bef)) → new_esEs19(xx3001, xx4001, bef)
new_esEs14(Just(xx3000), Just(xx4000), ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs4(xx300, xx400, app(ty_Maybe, bf)) → new_esEs14(xx300, xx400, bf)
new_esEs25(xx3000, xx4000, app(app(ty_Either, bch), bda)) → new_esEs16(xx3000, xx4000, bch, bda)
new_esEs22(xx3000, xx4000, ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs24(xx3002, xx4002, ty_Integer) → new_esEs6(xx3002, xx4002)
new_esEs4(xx300, xx400, ty_Int) → new_esEs9(xx300, xx400)
new_esEs11(xx3010, xx4010, app(ty_Maybe, bf)) → new_esEs14(xx3010, xx4010, bf)
new_esEs4(xx300, xx400, ty_Ordering) → new_esEs17(xx300, xx400)
new_primEqInt(Pos(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs13(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), bc, bd, be) → new_asAs(new_esEs22(xx3000, xx4000, bc), new_asAs(new_esEs23(xx3001, xx4001, bd), new_esEs24(xx3002, xx4002, be)))
new_esEs24(xx3002, xx4002, ty_Float) → new_esEs15(xx3002, xx4002)
new_esEs11(xx3010, xx4010, ty_Char) → new_esEs7(xx3010, xx4010)
new_esEs24(xx3002, xx4002, ty_@0) → new_esEs10(xx3002, xx4002)
new_esEs24(xx3002, xx4002, app(ty_Ratio, bcb)) → new_esEs19(xx3002, xx4002, bcb)
The set Q consists of the following terms:
new_esEs10(@0, @0)
new_esEs17(GT, LT)
new_esEs17(LT, GT)
new_esEs14(Just(x0), Just(x1), app(ty_[], x2))
new_esEs12(True, True)
new_esEs11(x0, x1, ty_Int)
new_esEs9(x0, x1)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Char)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs5([], [], x0)
new_esEs4(x0, x1, ty_Double)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Double)
new_esEs16(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Right(x0), Right(x1), x2, ty_Float)
new_esEs17(LT, LT)
new_esEs5([], :(x0, x1), x2)
new_esEs16(Left(x0), Left(x1), ty_@0, x2)
new_esEs25(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs24(x0, x1, ty_Bool)
new_esEs12(False, False)
new_primEqNat0(Succ(x0), Zero)
new_esEs14(Just(x0), Just(x1), ty_Ordering)
new_esEs7(Char(x0), Char(x1))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Float)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(x0, x1, ty_Float)
new_esEs16(Left(x0), Left(x1), ty_Double, x2)
new_esEs14(Just(x0), Just(x1), ty_Char)
new_esEs16(Left(x0), Left(x1), ty_Int, x2)
new_esEs26(x0, x1, ty_@0)
new_esEs11(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Char, x2)
new_esEs25(x0, x1, ty_Int)
new_esEs14(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(GT, EQ)
new_esEs17(EQ, GT)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs24(x0, x1, ty_Double)
new_esEs16(Right(x0), Right(x1), x2, ty_Integer)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs14(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs11(x0, x1, ty_Double)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primPlusNat1(Succ(x0), Zero)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_primPlusNat0(Succ(x0), x1)
new_esEs14(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Float)
new_esEs17(GT, GT)
new_esEs4(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, ty_Float)
new_esEs14(Just(x0), Just(x1), ty_Double)
new_esEs16(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs16(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Zero, Zero)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs4(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs16(Left(x0), Right(x1), x2, x3)
new_esEs16(Right(x0), Left(x1), x2, x3)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs14(Just(x0), Just(x1), ty_Float)
new_esEs24(x0, x1, ty_@0)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_@0)
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs11(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs14(Just(x0), Just(x1), ty_Int)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Zero)
new_esEs12(True, False)
new_esEs12(False, True)
new_esEs21(x0, x1, ty_Int)
new_esEs16(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs16(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs23(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs14(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Double)
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_esEs14(Nothing, Nothing, x0)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs25(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Right(x0), Right(x1), x2, ty_Bool)
new_esEs16(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs22(x0, x1, ty_@0)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Float)
new_esEs19(:%(x0, x1), :%(x2, x3), x4)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs14(Just(x0), Nothing, x1)
new_esEs24(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Float, x2)
new_esEs16(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs24(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, ty_Ordering)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqNat0(Zero, Succ(x0))
new_esEs5(:(x0, x1), [], x2)
new_esEs14(Just(x0), Just(x1), ty_@0)
new_esEs11(x0, x1, ty_@0)
new_esEs14(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat1(Zero, Zero)
new_esEs25(x0, x1, ty_Char)
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs14(Just(x0), Just(x1), ty_Integer)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs16(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs26(x0, x1, app(ty_[], x2))
new_asAs(True, x0)
new_esEs11(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Int)
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs16(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs4(x0, x1, ty_Float)
new_esEs17(EQ, EQ)
new_esEs14(Nothing, Just(x0), x1)
new_esEs6(Integer(x0), Integer(x1))
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Bool)
new_esEs14(Just(x0), Just(x1), ty_Bool)
new_esEs25(x0, x1, ty_Bool)
new_asAs(False, x0)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Integer)
new_esEs16(Right(x0), Right(x1), x2, ty_Int)
new_esEs23(x0, x1, ty_Double)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs0([], :(:(xx400, xx401), xx41), xx5, bb) → new_psPs0([], xx41, xx5, bb)
R is empty.
The set Q consists of the following terms:
new_esEs10(@0, @0)
new_esEs17(GT, LT)
new_esEs17(LT, GT)
new_esEs14(Just(x0), Just(x1), app(ty_[], x2))
new_esEs12(True, True)
new_esEs11(x0, x1, ty_Int)
new_esEs9(x0, x1)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Char)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs5([], [], x0)
new_esEs4(x0, x1, ty_Double)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Double)
new_esEs16(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Right(x0), Right(x1), x2, ty_Float)
new_esEs17(LT, LT)
new_esEs5([], :(x0, x1), x2)
new_esEs16(Left(x0), Left(x1), ty_@0, x2)
new_esEs25(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs24(x0, x1, ty_Bool)
new_esEs12(False, False)
new_primEqNat0(Succ(x0), Zero)
new_esEs14(Just(x0), Just(x1), ty_Ordering)
new_esEs7(Char(x0), Char(x1))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Float)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(x0, x1, ty_Float)
new_esEs16(Left(x0), Left(x1), ty_Double, x2)
new_esEs14(Just(x0), Just(x1), ty_Char)
new_esEs16(Left(x0), Left(x1), ty_Int, x2)
new_esEs26(x0, x1, ty_@0)
new_esEs11(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Char, x2)
new_esEs25(x0, x1, ty_Int)
new_esEs14(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(GT, EQ)
new_esEs17(EQ, GT)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs24(x0, x1, ty_Double)
new_esEs16(Right(x0), Right(x1), x2, ty_Integer)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs14(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs11(x0, x1, ty_Double)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primPlusNat1(Succ(x0), Zero)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_primPlusNat0(Succ(x0), x1)
new_esEs14(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Float)
new_esEs17(GT, GT)
new_esEs4(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, ty_Float)
new_esEs14(Just(x0), Just(x1), ty_Double)
new_esEs16(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs16(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Zero, Zero)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs4(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs16(Left(x0), Right(x1), x2, x3)
new_esEs16(Right(x0), Left(x1), x2, x3)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs14(Just(x0), Just(x1), ty_Float)
new_esEs24(x0, x1, ty_@0)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_@0)
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs11(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs14(Just(x0), Just(x1), ty_Int)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Zero)
new_esEs12(True, False)
new_esEs12(False, True)
new_esEs21(x0, x1, ty_Int)
new_esEs16(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs16(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs23(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs14(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Double)
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_esEs14(Nothing, Nothing, x0)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs25(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Right(x0), Right(x1), x2, ty_Bool)
new_esEs16(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs22(x0, x1, ty_@0)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Float)
new_esEs19(:%(x0, x1), :%(x2, x3), x4)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs14(Just(x0), Nothing, x1)
new_esEs24(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Float, x2)
new_esEs16(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs24(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, ty_Ordering)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqNat0(Zero, Succ(x0))
new_esEs5(:(x0, x1), [], x2)
new_esEs14(Just(x0), Just(x1), ty_@0)
new_esEs11(x0, x1, ty_@0)
new_esEs14(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat1(Zero, Zero)
new_esEs25(x0, x1, ty_Char)
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs14(Just(x0), Just(x1), ty_Integer)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs16(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs26(x0, x1, app(ty_[], x2))
new_asAs(True, x0)
new_esEs11(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Int)
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs16(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs4(x0, x1, ty_Float)
new_esEs17(EQ, EQ)
new_esEs14(Nothing, Just(x0), x1)
new_esEs6(Integer(x0), Integer(x1))
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Bool)
new_esEs14(Just(x0), Just(x1), ty_Bool)
new_esEs25(x0, x1, ty_Bool)
new_asAs(False, x0)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Integer)
new_esEs16(Right(x0), Right(x1), x2, ty_Int)
new_esEs23(x0, x1, ty_Double)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_esEs10(@0, @0)
new_esEs17(GT, LT)
new_esEs17(LT, GT)
new_esEs14(Just(x0), Just(x1), app(ty_[], x2))
new_esEs12(True, True)
new_esEs11(x0, x1, ty_Int)
new_esEs9(x0, x1)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Char)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs5([], [], x0)
new_esEs4(x0, x1, ty_Double)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Double)
new_esEs16(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Right(x0), Right(x1), x2, ty_Float)
new_esEs17(LT, LT)
new_esEs5([], :(x0, x1), x2)
new_esEs16(Left(x0), Left(x1), ty_@0, x2)
new_esEs25(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs24(x0, x1, ty_Bool)
new_esEs12(False, False)
new_primEqNat0(Succ(x0), Zero)
new_esEs14(Just(x0), Just(x1), ty_Ordering)
new_esEs7(Char(x0), Char(x1))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Float)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(x0, x1, ty_Float)
new_esEs16(Left(x0), Left(x1), ty_Double, x2)
new_esEs14(Just(x0), Just(x1), ty_Char)
new_esEs16(Left(x0), Left(x1), ty_Int, x2)
new_esEs26(x0, x1, ty_@0)
new_esEs11(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Char, x2)
new_esEs25(x0, x1, ty_Int)
new_esEs14(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(GT, EQ)
new_esEs17(EQ, GT)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs24(x0, x1, ty_Double)
new_esEs16(Right(x0), Right(x1), x2, ty_Integer)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs14(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs11(x0, x1, ty_Double)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primPlusNat1(Succ(x0), Zero)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_primPlusNat0(Succ(x0), x1)
new_esEs14(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Float)
new_esEs17(GT, GT)
new_esEs4(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, ty_Float)
new_esEs14(Just(x0), Just(x1), ty_Double)
new_esEs16(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs16(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Zero, Zero)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs4(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs16(Left(x0), Right(x1), x2, x3)
new_esEs16(Right(x0), Left(x1), x2, x3)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs14(Just(x0), Just(x1), ty_Float)
new_esEs24(x0, x1, ty_@0)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_@0)
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs11(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs14(Just(x0), Just(x1), ty_Int)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Zero)
new_esEs12(True, False)
new_esEs12(False, True)
new_esEs21(x0, x1, ty_Int)
new_esEs16(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs16(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs23(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs14(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Double)
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_esEs14(Nothing, Nothing, x0)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs25(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Right(x0), Right(x1), x2, ty_Bool)
new_esEs16(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs22(x0, x1, ty_@0)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Float)
new_esEs19(:%(x0, x1), :%(x2, x3), x4)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs14(Just(x0), Nothing, x1)
new_esEs24(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Float, x2)
new_esEs16(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs24(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, ty_Ordering)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqNat0(Zero, Succ(x0))
new_esEs5(:(x0, x1), [], x2)
new_esEs14(Just(x0), Just(x1), ty_@0)
new_esEs11(x0, x1, ty_@0)
new_esEs14(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat1(Zero, Zero)
new_esEs25(x0, x1, ty_Char)
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs14(Just(x0), Just(x1), ty_Integer)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs16(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs26(x0, x1, app(ty_[], x2))
new_asAs(True, x0)
new_esEs11(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Int)
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs16(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs4(x0, x1, ty_Float)
new_esEs17(EQ, EQ)
new_esEs14(Nothing, Just(x0), x1)
new_esEs6(Integer(x0), Integer(x1))
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Bool)
new_esEs14(Just(x0), Just(x1), ty_Bool)
new_esEs25(x0, x1, ty_Bool)
new_asAs(False, x0)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Integer)
new_esEs16(Right(x0), Right(x1), x2, ty_Int)
new_esEs23(x0, x1, ty_Double)
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs0([], :(:(xx400, xx401), xx41), xx5, bb) → new_psPs0([], xx41, xx5, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs0([], :(:(xx400, xx401), xx41), xx5, bb) → new_psPs0([], xx41, xx5, bb)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3, 4 >= 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs0(:(xx300, xx301), :([], xx41), xx5, bb) → new_psPs(xx300, xx301, False, xx41, xx5, bb)
new_psPs0(:(xx300, xx301), :(:(xx400, xx401), xx41), xx5, bb) → new_psPs(xx300, xx301, new_asAs(new_esEs4(xx300, xx400, bb), new_esEs5(xx301, xx401, bb)), xx41, xx5, bb)
new_psPs(xx13, xx14, False, xx17, xx18, ba) → new_psPs0(:(xx13, xx14), xx17, xx18, ba)
The TRS R consists of the following rules:
new_esEs25(xx3000, xx4000, ty_Ordering) → new_esEs17(xx3000, xx4000)
new_esEs14(Just(xx3000), Just(xx4000), ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Double, ca) → new_esEs8(xx3000, xx4000)
new_esEs25(xx3000, xx4000, app(ty_Maybe, bcf)) → new_esEs14(xx3000, xx4000, bcf)
new_primPlusNat1(Succ(xx3300), Succ(xx4000000)) → Succ(Succ(new_primPlusNat1(xx3300, xx4000000)))
new_primEqInt(Pos(Succ(xx30000)), Neg(xx4000)) → False
new_primEqInt(Neg(Succ(xx30000)), Pos(xx4000)) → False
new_esEs23(xx3001, xx4001, app(app(ty_@2, baf), bag)) → new_esEs18(xx3001, xx4001, baf, bag)
new_esEs4(xx300, xx400, ty_Bool) → new_esEs12(xx300, xx400)
new_esEs7(Char(xx3000), Char(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Bool, ca) → new_esEs12(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), app(ty_Maybe, da), ca) → new_esEs14(xx3000, xx4000, da)
new_esEs26(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_primEqInt(Pos(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xx40000))) → False
new_esEs16(Left(xx3000), Left(xx4000), app(ty_Ratio, dg), ca) → new_esEs19(xx3000, xx4000, dg)
new_esEs4(xx300, xx400, app(app(app(ty_@3, bc), bd), be)) → new_esEs13(xx300, xx400, bc, bd, be)
new_esEs5([], [], bb) → True
new_esEs11(xx3010, xx4010, app(ty_[], bg)) → new_esEs5(xx3010, xx4010, bg)
new_esEs20(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs14(Just(xx3000), Just(xx4000), ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs23(xx3001, xx4001, app(ty_Maybe, bab)) → new_esEs14(xx3001, xx4001, bab)
new_esEs25(xx3000, xx4000, ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_@0) → new_esEs10(xx3010, xx4010)
new_esEs22(xx3000, xx4000, ty_Integer) → new_esEs6(xx3000, xx4000)
new_primMulNat0(Zero, Zero) → Zero
new_esEs22(xx3000, xx4000, ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3001, xx4001, ty_Float) → new_esEs15(xx3001, xx4001)
new_esEs4(xx300, xx400, ty_@0) → new_esEs10(xx300, xx400)
new_esEs12(True, True) → True
new_esEs5([], :(xx4010, xx4011), bb) → False
new_esEs5(:(xx3010, xx3011), [], bb) → False
new_esEs25(xx3000, xx4000, ty_Double) → new_esEs8(xx3000, xx4000)
new_primPlusNat0(Zero, xx400000) → Succ(xx400000)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs6(Integer(xx3000), Integer(xx4000)) → new_primEqInt(xx3000, xx4000)
new_esEs23(xx3001, xx4001, ty_Bool) → new_esEs12(xx3001, xx4001)
new_esEs4(xx300, xx400, ty_Float) → new_esEs15(xx300, xx400)
new_sr(Pos(xx30000), Neg(xx40000)) → Neg(new_primMulNat0(xx30000, xx40000))
new_sr(Neg(xx30000), Pos(xx40000)) → Neg(new_primMulNat0(xx30000, xx40000))
new_esEs23(xx3001, xx4001, ty_@0) → new_esEs10(xx3001, xx4001)
new_esEs14(Just(xx3000), Just(xx4000), ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs22(xx3000, xx4000, app(ty_Ratio, hf)) → new_esEs19(xx3000, xx4000, hf)
new_esEs15(Float(xx3000, xx3001), Float(xx4000, xx4001)) → new_esEs9(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs16(Right(xx3000), Right(xx4000), bh, app(app(ty_Either, ee), ef)) → new_esEs16(xx3000, xx4000, ee, ef)
new_esEs24(xx3002, xx4002, ty_Char) → new_esEs7(xx3002, xx4002)
new_esEs26(xx3001, xx4001, ty_Double) → new_esEs8(xx3001, xx4001)
new_esEs16(Left(xx3000), Left(xx4000), ty_Int, ca) → new_esEs9(xx3000, xx4000)
new_esEs18(@2(xx3000, xx3001), @2(xx4000, xx4001), cb, cc) → new_asAs(new_esEs25(xx3000, xx4000, cb), new_esEs26(xx3001, xx4001, cc))
new_esEs11(xx3010, xx4010, app(app(ty_Either, bh), ca)) → new_esEs16(xx3010, xx4010, bh, ca)
new_esEs26(xx3001, xx4001, app(app(ty_@2, bed), bee)) → new_esEs18(xx3001, xx4001, bed, bee)
new_esEs26(xx3001, xx4001, ty_@0) → new_esEs10(xx3001, xx4001)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(ty_[], ed)) → new_esEs5(xx3000, xx4000, ed)
new_esEs26(xx3001, xx4001, ty_Integer) → new_esEs6(xx3001, xx4001)
new_esEs22(xx3000, xx4000, app(app(ty_@2, hd), he)) → new_esEs18(xx3000, xx4000, hd, he)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(ty_Maybe, ec)) → new_esEs14(xx3000, xx4000, ec)
new_primEqNat0(Zero, Succ(xx40000)) → False
new_primEqNat0(Succ(xx30000), Zero) → False
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Double) → new_esEs8(xx3000, xx4000)
new_esEs21(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_esEs24(xx3002, xx4002, app(ty_Maybe, bbd)) → new_esEs14(xx3002, xx4002, bbd)
new_esEs4(xx300, xx400, app(ty_[], bg)) → new_esEs5(xx300, xx400, bg)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Ordering) → new_esEs17(xx3000, xx4000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs26(xx3001, xx4001, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs13(xx3001, xx4001, bde, bdf, bdg)
new_esEs23(xx3001, xx4001, ty_Integer) → new_esEs6(xx3001, xx4001)
new_esEs22(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Float, ca) → new_esEs15(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Bool) → new_esEs12(xx3010, xx4010)
new_esEs23(xx3001, xx4001, ty_Double) → new_esEs8(xx3001, xx4001)
new_esEs4(xx300, xx400, app(ty_Ratio, cd)) → new_esEs19(xx300, xx400, cd)
new_esEs22(xx3000, xx4000, ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), app(app(ty_Either, dc), dd), ca) → new_esEs16(xx3000, xx4000, dc, dd)
new_esEs26(xx3001, xx4001, ty_Bool) → new_esEs12(xx3001, xx4001)
new_esEs23(xx3001, xx4001, app(ty_[], bac)) → new_esEs5(xx3001, xx4001, bac)
new_esEs24(xx3002, xx4002, ty_Int) → new_esEs9(xx3002, xx4002)
new_esEs16(Left(xx3000), Right(xx4000), bh, ca) → False
new_esEs16(Right(xx3000), Left(xx4000), bh, ca) → False
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs16(Left(xx3000), Left(xx4000), app(ty_[], db), ca) → new_esEs5(xx3000, xx4000, db)
new_esEs19(:%(xx3000, xx3001), :%(xx4000, xx4001), cd) → new_asAs(new_esEs20(xx3000, xx4000, cd), new_esEs21(xx3001, xx4001, cd))
new_esEs25(xx3000, xx4000, ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs4(xx300, xx400, app(app(ty_@2, cb), cc)) → new_esEs18(xx300, xx400, cb, cc)
new_esEs23(xx3001, xx4001, ty_Char) → new_esEs7(xx3001, xx4001)
new_esEs22(xx3000, xx4000, ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs4(xx300, xx400, ty_Integer) → new_esEs6(xx300, xx400)
new_esEs23(xx3001, xx4001, ty_Ordering) → new_esEs17(xx3001, xx4001)
new_esEs17(LT, LT) → True
new_esEs14(Just(xx3000), Just(xx4000), app(ty_[], fg)) → new_esEs5(xx3000, xx4000, fg)
new_esEs5(:(xx3010, xx3011), :(xx4010, xx4011), bb) → new_asAs(new_esEs11(xx3010, xx4010, bb), new_esEs5(xx3011, xx4011, bb))
new_esEs22(xx3000, xx4000, app(ty_[], ha)) → new_esEs5(xx3000, xx4000, ha)
new_esEs14(Just(xx3000), Just(xx4000), app(app(ty_@2, gb), gc)) → new_esEs18(xx3000, xx4000, gb, gc)
new_esEs10(@0, @0) → True
new_esEs25(xx3000, xx4000, ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs11(xx3010, xx4010, app(app(app(ty_@3, bc), bd), be)) → new_esEs13(xx3010, xx4010, bc, bd, be)
new_sr(Neg(xx30000), Neg(xx40000)) → Pos(new_primMulNat0(xx30000, xx40000))
new_esEs14(Nothing, Nothing, bf) → True
new_asAs(False, xx32) → False
new_sr(Pos(xx30000), Pos(xx40000)) → Pos(new_primMulNat0(xx30000, xx40000))
new_esEs25(xx3000, xx4000, app(ty_[], bcg)) → new_esEs5(xx3000, xx4000, bcg)
new_esEs14(Just(xx3000), Just(xx4000), ty_Double) → new_esEs8(xx3000, xx4000)
new_primEqNat0(Zero, Zero) → True
new_esEs16(Left(xx3000), Left(xx4000), ty_Integer, ca) → new_esEs6(xx3000, xx4000)
new_primMulNat0(Zero, Succ(xx400000)) → Zero
new_primMulNat0(Succ(xx300000), Zero) → Zero
new_esEs14(Just(xx3000), Just(xx4000), ty_Ordering) → new_esEs17(xx3000, xx4000)
new_esEs25(xx3000, xx4000, ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs23(xx3001, xx4001, ty_Int) → new_esEs9(xx3001, xx4001)
new_esEs23(xx3001, xx4001, app(app(app(ty_@3, hg), hh), baa)) → new_esEs13(xx3001, xx4001, hg, hh, baa)
new_esEs22(xx3000, xx4000, app(app(ty_Either, hb), hc)) → new_esEs16(xx3000, xx4000, hb, hc)
new_esEs22(xx3000, xx4000, app(app(app(ty_@3, ge), gf), gg)) → new_esEs13(xx3000, xx4000, ge, gf, gg)
new_esEs16(Left(xx3000), Left(xx4000), ty_Ordering, ca) → new_esEs17(xx3000, xx4000)
new_esEs23(xx3001, xx4001, ty_Float) → new_esEs15(xx3001, xx4001)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Float) → new_esEs15(xx3000, xx4000)
new_esEs14(Just(xx3000), Just(xx4000), ty_Char) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3001, xx4001, ty_Char) → new_esEs7(xx3001, xx4001)
new_esEs26(xx3001, xx4001, app(app(ty_Either, beb), bec)) → new_esEs16(xx3001, xx4001, beb, bec)
new_esEs14(Just(xx3000), Just(xx4000), app(ty_Maybe, ff)) → new_esEs14(xx3000, xx4000, ff)
new_esEs11(xx3010, xx4010, ty_Double) → new_esEs8(xx3010, xx4010)
new_esEs24(xx3002, xx4002, ty_Bool) → new_esEs12(xx3002, xx4002)
new_esEs23(xx3001, xx4001, app(ty_Ratio, bah)) → new_esEs19(xx3001, xx4001, bah)
new_esEs24(xx3002, xx4002, app(ty_[], bbe)) → new_esEs5(xx3002, xx4002, bbe)
new_esEs23(xx3001, xx4001, app(app(ty_Either, bad), bae)) → new_esEs16(xx3001, xx4001, bad, bae)
new_esEs25(xx3000, xx4000, ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs26(xx3001, xx4001, app(ty_[], bea)) → new_esEs5(xx3001, xx4001, bea)
new_esEs11(xx3010, xx4010, app(ty_Ratio, cd)) → new_esEs19(xx3010, xx4010, cd)
new_primPlusNat0(Succ(xx330), xx400000) → Succ(Succ(new_primPlusNat1(xx330, xx400000)))
new_esEs17(LT, EQ) → False
new_esEs14(Just(xx3000), Just(xx4000), app(app(ty_Either, fh), ga)) → new_esEs16(xx3000, xx4000, fh, ga)
new_esEs17(EQ, LT) → False
new_esEs12(False, False) → True
new_esEs12(False, True) → False
new_esEs12(True, False) → False
new_esEs25(xx3000, xx4000, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs13(xx3000, xx4000, bcc, bcd, bce)
new_esEs14(Just(xx3000), Just(xx4000), app(app(app(ty_@3, fb), fc), fd)) → new_esEs13(xx3000, xx4000, fb, fc, fd)
new_esEs14(Just(xx3000), Nothing, bf) → False
new_esEs14(Nothing, Just(xx4000), bf) → False
new_primEqInt(Neg(Succ(xx30000)), Neg(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs24(xx3002, xx4002, ty_Double) → new_esEs8(xx3002, xx4002)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(app(ty_@2, eg), eh)) → new_esEs18(xx3000, xx4000, eg, eh)
new_esEs4(xx300, xx400, ty_Char) → new_esEs7(xx300, xx400)
new_esEs14(Just(xx3000), Just(xx4000), ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs25(xx3000, xx4000, app(app(ty_@2, bdb), bdc)) → new_esEs18(xx3000, xx4000, bdb, bdc)
new_esEs24(xx3002, xx4002, app(app(ty_@2, bbh), bca)) → new_esEs18(xx3002, xx4002, bbh, bca)
new_esEs24(xx3002, xx4002, ty_Ordering) → new_esEs17(xx3002, xx4002)
new_esEs4(xx300, xx400, ty_Double) → new_esEs8(xx300, xx400)
new_primPlusNat1(Succ(xx3300), Zero) → Succ(xx3300)
new_primPlusNat1(Zero, Succ(xx4000000)) → Succ(xx4000000)
new_esEs16(Right(xx3000), Right(xx4000), bh, app(ty_Ratio, fa)) → new_esEs19(xx3000, xx4000, fa)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs8(Double(xx3000, xx3001), Double(xx4000, xx4001)) → new_esEs9(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs26(xx3001, xx4001, ty_Ordering) → new_esEs17(xx3001, xx4001)
new_esEs16(Left(xx3000), Left(xx4000), ty_@0, ca) → new_esEs10(xx3000, xx4000)
new_esEs22(xx3000, xx4000, ty_Ordering) → new_esEs17(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Int) → new_esEs9(xx3010, xx4010)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs14(Just(xx3000), Just(xx4000), app(ty_Ratio, gd)) → new_esEs19(xx3000, xx4000, gd)
new_esEs17(EQ, EQ) → True
new_esEs4(xx300, xx400, app(app(ty_Either, bh), ca)) → new_esEs16(xx300, xx400, bh, ca)
new_esEs24(xx3002, xx4002, app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs13(xx3002, xx4002, bba, bbb, bbc)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs26(xx3001, xx4001, app(ty_Maybe, bdh)) → new_esEs14(xx3001, xx4001, bdh)
new_esEs11(xx3010, xx4010, ty_Float) → new_esEs15(xx3010, xx4010)
new_primEqInt(Neg(Succ(xx30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xx40000))) → False
new_esEs16(Right(xx3000), Right(xx4000), bh, app(app(app(ty_@3, dh), ea), eb)) → new_esEs13(xx3000, xx4000, dh, ea, eb)
new_esEs20(xx3000, xx4000, ty_Integer) → new_esEs6(xx3000, xx4000)
new_esEs21(xx3001, xx4001, ty_Integer) → new_esEs6(xx3001, xx4001)
new_esEs22(xx3000, xx4000, app(ty_Maybe, gh)) → new_esEs14(xx3000, xx4000, gh)
new_esEs25(xx3000, xx4000, app(ty_Ratio, bdd)) → new_esEs19(xx3000, xx4000, bdd)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs16(Left(xx3000), Left(xx4000), app(app(app(ty_@3, ce), cf), cg), ca) → new_esEs13(xx3000, xx4000, ce, cf, cg)
new_asAs(True, xx32) → xx32
new_esEs16(Left(xx3000), Left(xx4000), app(app(ty_@2, de), df), ca) → new_esEs18(xx3000, xx4000, de, df)
new_primMulNat0(Succ(xx300000), Succ(xx400000)) → new_primPlusNat0(new_primMulNat0(xx300000, Succ(xx400000)), xx400000)
new_esEs17(GT, GT) → True
new_esEs22(xx3000, xx4000, ty_Double) → new_esEs8(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Integer) → new_esEs6(xx3010, xx4010)
new_primEqInt(Pos(Succ(xx30000)), Pos(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs16(Left(xx3000), Left(xx4000), ty_Char, ca) → new_esEs7(xx3000, xx4000)
new_esEs11(xx3010, xx4010, ty_Ordering) → new_esEs17(xx3010, xx4010)
new_esEs16(Right(xx3000), Right(xx4000), bh, ty_@0) → new_esEs10(xx3000, xx4000)
new_esEs25(xx3000, xx4000, ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs17(LT, GT) → False
new_esEs17(GT, LT) → False
new_esEs11(xx3010, xx4010, app(app(ty_@2, cb), cc)) → new_esEs18(xx3010, xx4010, cb, cc)
new_esEs24(xx3002, xx4002, app(app(ty_Either, bbf), bbg)) → new_esEs16(xx3002, xx4002, bbf, bbg)
new_primEqNat0(Succ(xx30000), Succ(xx40000)) → new_primEqNat0(xx30000, xx40000)
new_esEs17(EQ, GT) → False
new_esEs17(GT, EQ) → False
new_esEs9(xx300, xx400) → new_primEqInt(xx300, xx400)
new_esEs26(xx3001, xx4001, app(ty_Ratio, bef)) → new_esEs19(xx3001, xx4001, bef)
new_esEs14(Just(xx3000), Just(xx4000), ty_Int) → new_esEs9(xx3000, xx4000)
new_esEs4(xx300, xx400, app(ty_Maybe, bf)) → new_esEs14(xx300, xx400, bf)
new_esEs25(xx3000, xx4000, app(app(ty_Either, bch), bda)) → new_esEs16(xx3000, xx4000, bch, bda)
new_esEs22(xx3000, xx4000, ty_Bool) → new_esEs12(xx3000, xx4000)
new_esEs24(xx3002, xx4002, ty_Integer) → new_esEs6(xx3002, xx4002)
new_esEs4(xx300, xx400, ty_Int) → new_esEs9(xx300, xx400)
new_esEs11(xx3010, xx4010, app(ty_Maybe, bf)) → new_esEs14(xx3010, xx4010, bf)
new_esEs4(xx300, xx400, ty_Ordering) → new_esEs17(xx300, xx400)
new_primEqInt(Pos(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_esEs13(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), bc, bd, be) → new_asAs(new_esEs22(xx3000, xx4000, bc), new_asAs(new_esEs23(xx3001, xx4001, bd), new_esEs24(xx3002, xx4002, be)))
new_esEs24(xx3002, xx4002, ty_Float) → new_esEs15(xx3002, xx4002)
new_esEs11(xx3010, xx4010, ty_Char) → new_esEs7(xx3010, xx4010)
new_esEs24(xx3002, xx4002, ty_@0) → new_esEs10(xx3002, xx4002)
new_esEs24(xx3002, xx4002, app(ty_Ratio, bcb)) → new_esEs19(xx3002, xx4002, bcb)
The set Q consists of the following terms:
new_esEs10(@0, @0)
new_esEs17(GT, LT)
new_esEs17(LT, GT)
new_esEs14(Just(x0), Just(x1), app(ty_[], x2))
new_esEs12(True, True)
new_esEs11(x0, x1, ty_Int)
new_esEs9(x0, x1)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Char)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs5([], [], x0)
new_esEs4(x0, x1, ty_Double)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Double)
new_esEs16(Left(x0), Left(x1), ty_Integer, x2)
new_esEs16(Right(x0), Right(x1), x2, ty_Float)
new_esEs17(LT, LT)
new_esEs5([], :(x0, x1), x2)
new_esEs16(Left(x0), Left(x1), ty_@0, x2)
new_esEs25(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs24(x0, x1, ty_Bool)
new_esEs12(False, False)
new_primEqNat0(Succ(x0), Zero)
new_esEs14(Just(x0), Just(x1), ty_Ordering)
new_esEs7(Char(x0), Char(x1))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Float)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(x0, x1, ty_Float)
new_esEs16(Left(x0), Left(x1), ty_Double, x2)
new_esEs14(Just(x0), Just(x1), ty_Char)
new_esEs16(Left(x0), Left(x1), ty_Int, x2)
new_esEs26(x0, x1, ty_@0)
new_esEs11(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Char, x2)
new_esEs25(x0, x1, ty_Int)
new_esEs14(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(GT, EQ)
new_esEs17(EQ, GT)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs24(x0, x1, ty_Double)
new_esEs16(Right(x0), Right(x1), x2, ty_Integer)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs14(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs11(x0, x1, ty_Double)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primPlusNat1(Succ(x0), Zero)
new_esEs16(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Zero, x0)
new_primPlusNat0(Succ(x0), x1)
new_esEs14(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Float)
new_esEs17(GT, GT)
new_esEs4(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Float)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Left(x0), Left(x1), ty_Bool, x2)
new_esEs24(x0, x1, ty_Float)
new_esEs14(Just(x0), Just(x1), ty_Double)
new_esEs16(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs16(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqNat0(Zero, Zero)
new_esEs8(Double(x0, x1), Double(x2, x3))
new_esEs4(x0, x1, ty_@0)
new_esEs21(x0, x1, ty_Integer)
new_esEs16(Left(x0), Right(x1), x2, x3)
new_esEs16(Right(x0), Left(x1), x2, x3)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Ordering)
new_esEs16(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs14(Just(x0), Just(x1), ty_Float)
new_esEs24(x0, x1, ty_@0)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, ty_@0)
new_esEs23(x0, x1, app(ty_[], x2))
new_primMulNat0(Succ(x0), Zero)
new_esEs11(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs22(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs15(Float(x0, x1), Float(x2, x3))
new_esEs14(Just(x0), Just(x1), ty_Int)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Zero, Zero)
new_esEs12(True, False)
new_esEs12(False, True)
new_esEs21(x0, x1, ty_Int)
new_esEs16(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs16(Right(x0), Right(x1), x2, ty_Double)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs23(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Char)
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs14(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Double)
new_esEs11(x0, x1, app(ty_Maybe, x2))
new_esEs14(Nothing, Nothing, x0)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs11(x0, x1, app(ty_[], x2))
new_esEs11(x0, x1, app(ty_Ratio, x2))
new_esEs16(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_esEs25(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Right(x0), Right(x1), x2, ty_Bool)
new_esEs16(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs22(x0, x1, ty_@0)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs11(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Float)
new_esEs19(:%(x0, x1), :%(x2, x3), x4)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs14(Just(x0), Nothing, x1)
new_esEs24(x0, x1, ty_Ordering)
new_esEs16(Left(x0), Left(x1), ty_Float, x2)
new_esEs16(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs24(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs11(x0, x1, ty_Ordering)
new_sr(Pos(x0), Pos(x1))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqNat0(Zero, Succ(x0))
new_esEs5(:(x0, x1), [], x2)
new_esEs14(Just(x0), Just(x1), ty_@0)
new_esEs11(x0, x1, ty_@0)
new_esEs14(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat1(Zero, Zero)
new_esEs25(x0, x1, ty_Char)
new_esEs11(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs14(Just(x0), Just(x1), ty_Integer)
new_esEs11(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs16(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs26(x0, x1, app(ty_[], x2))
new_asAs(True, x0)
new_esEs11(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Int)
new_esEs18(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs16(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs4(x0, x1, ty_Float)
new_esEs17(EQ, EQ)
new_esEs14(Nothing, Just(x0), x1)
new_esEs6(Integer(x0), Integer(x1))
new_esEs17(EQ, LT)
new_esEs17(LT, EQ)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs24(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Bool)
new_esEs14(Just(x0), Just(x1), ty_Bool)
new_esEs25(x0, x1, ty_Bool)
new_asAs(False, x0)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_Integer)
new_esEs16(Right(x0), Right(x1), x2, ty_Int)
new_esEs23(x0, x1, ty_Double)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs(xx13, xx14, False, xx17, xx18, ba) → new_psPs0(:(xx13, xx14), xx17, xx18, ba)
The graph contains the following edges 4 >= 2, 5 >= 3, 6 >= 4
- new_psPs0(:(xx300, xx301), :([], xx41), xx5, bb) → new_psPs(xx300, xx301, False, xx41, xx5, bb)
The graph contains the following edges 1 > 1, 1 > 2, 2 > 4, 3 >= 5, 4 >= 6
- new_psPs0(:(xx300, xx301), :(:(xx400, xx401), xx41), xx5, bb) → new_psPs(xx300, xx301, new_asAs(new_esEs4(xx300, xx400, bb), new_esEs5(xx301, xx401, bb)), xx41, xx5, bb)
The graph contains the following edges 1 > 1, 1 > 2, 2 > 4, 3 >= 5, 4 >= 6
↳ HASKELL
↳ LR
↳ HASKELL
↳ CR
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_foldr(xx4, :(xx30, xx31), ba) → new_foldr(xx4, xx31, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_foldr(xx4, :(xx30, xx31), ba) → new_foldr(xx4, xx31, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3